(set-logic QF_UFNIA)
(declare-const i1 Int)
(declare-const i8 Int)
(declare-const i10 Int)
(declare-const i11 Int)
(declare-const i12 Int)
(declare-const i13 Int)
(declare-const i14 Int)
(declare-const i15 Int)
(declare-const i16 Int)
(declare-const i17 Int)
(declare-const i18 Int)
(declare-const i19 Int)
(declare-const i20 Int)
(declare-const i21 Int)
(declare-const i22 Int)
(declare-const i23 Int)
(declare-const i24 Int)
(declare-const i25 Int)
(declare-const i26 Int)
(declare-const i27 Int)
(declare-const i28 Int)
(declare-const i29 Int)
(assert (or (>= 502 (* 51 (* 57 11 855 i1 64) 6) (- 583) (* 51 (* 57 11 855 i1 64) 6)) (>= 502 (* 51 (* 57 11 855 i1 64) 6) (- 583) (* 51 (* 57 11 855 i1 64) 6)) (= 789 (mod i15 64))))
(check-sat-assuming-model (i1 i8 i10 i11 i12 i13 i14 i15 i16 i17 i18 i19 i20 i21 i22 i23 i24 i25 i26 i27 i28 i29 ) (39126 17561 11795 35909 27486 41578 11592 2309 39634 27389 27820 48068 26387 10418 7418 22354 28089 5323 38299 3609 6675 38654 ))
